<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>Host Dependencies | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/projects/">
              <span property="name"><b>Projects</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/projects/buildsystem/">
              <span property="name"><b>System configuration and building</b></span>
            </a>
            <meta property="position" content="3" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">Host Dependencies</span>
            <meta property="position" content="4" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    


<div class="sidebar">



      <ul class="nav nav-sidebar">
  
        <li class="">
          <a class="" href="/Resources.html">
            Resources
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/sel4/documentation.html">
            seL4 Documentation
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/sel4/frequently-asked-questions.html">
            seL4 FAQ
          </a>
        </li>
  
        <li class="active">
          <a class="" href="/projects/buildsystem/host-dependencies.html">
            Set up your machine
          </a>
        </li>
  
        <li class="">
          <a class="" href="/Hardware/">
            Supported platforms
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/available-user-components.html">
            Available components
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/roadmap.html">
            Roadmap
          </a>
        </li>
  
        <li class="">
          <a class="" href="/CommunityProjects.html">
            Community projects
          </a>
        </li>
  
        <li class="">
          <a class="" href="/releases/sel4">
            Release Notes
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/sel4/api-doc.html">
            libsel4 API
          </a>
        </li>
  
        <li class="">
          <a class="" href="https://sel4.systems/Info/Docs/seL4-manual-latest.pdf">
            Current Manual
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/sel4/verified-configurations.html">
            Verified Configurations
          </a>
        </li>
  
      </ul>














</div>

  </div>
  <div class="content col-sm-8 col-md-6 col-lg-7 main">
    <h1 id="host-dependencies">Host Dependencies</h1>

<p>This page describes how to set up your host machine to build and run seL4 and its supported projects. To compile and use seL4 you can either:</p>

<ul>
  <li><em>Recommended:</em> Use Docker to isolate the dependencies from your machine. Detailed instructions for using Docker for building seL4, Camkes, and L4v can be found <a href="/projects/dockerfiles/">here</a>.</li>
  <li>Install the following dependencies on your local OS</li>
</ul>

<p>The following instructions describe how to set up the required dependencies on your local OS. This page assumes you are building in a Linux OS. We however encourage site <a href="https://docs.sel4.systems/DocsContributing">contributions</a> for building in alternative OSes (e.g. macOS).</p>

<h2 id="get-googles-repo-tool">Get Google’s Repo tool</h2>

<p>The primary way of obtaining and managing seL4 project source is through the use of Google’s repo tool. To get repo, follow the instructions described in the section “Install” <a href="https://gerrit.googlesource.com/git-repo#install">here</a>.</p>

<p>See the <a href="repo-cheatsheet">RepoCheatsheet</a> page for a quick explanation of how we use Repo.</p>

<h2 id="sel4-build-dependencies">seL4 Build Dependencies</h2>

<p>To build seL4-based projects, ensure you have installed the dependencies described in the <a href="#base-build-dependencies">Base Build Dependencies</a> and <a href="#python-dependencies">Python Dependencies</a> sections below.</p>

<h3 id="base-build-dependencies">Base Build Dependencies</h3>

<p>To establish a usable development environment it is important to install your distributions basic build packages.</p>

<h4 id="ubuntu">Ubuntu</h4>

<p>These instructions are intended for Ubuntu LTS versions 20.04 and 22.04.</p>

<blockquote>
  <p>As dependencies and packages may be frequently changed, deprecated or updated these instructions may become out of date. If you discover any missing dependencies and packages we welcome new <a href="https://docs.sel4.systems/DocsContributing">contributions</a> to the page.</p>
</blockquote>

<p><strong>Base dependencies</strong></p>

<p>The basic build package on Ubuntu is the <code class="language-plaintext highlighter-rouge">build-essential</code> package. To install run:</p>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">sudo </span>apt-get update
<span class="nb">sudo </span>apt-get <span class="nb">install </span>build-essential
</code></pre></div></div>

<p>Additional base dependencies for building seL4 projects on Ubuntu include installing:</p>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">sudo </span>apt-get <span class="nb">install </span>cmake ccache ninja-build cmake-curses-gui
<span class="nb">sudo </span>apt-get <span class="nb">install </span>libxml2-utils ncurses-dev
<span class="nb">sudo </span>apt-get <span class="nb">install </span>curl git doxygen device-tree-compiler
<span class="nb">sudo </span>apt-get <span class="nb">install </span>u-boot-tools
<span class="nb">sudo </span>apt-get <span class="nb">install </span>python3-dev python3-pip python-is-python3
<span class="nb">sudo </span>apt-get <span class="nb">install </span>protobuf-compiler python3-protobuf
</code></pre></div></div>

<p><strong>Simulating with QEMU</strong></p>

<p>In order to run seL4 projects on a simulator you will need QEMU:</p>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">sudo </span>apt-get <span class="nb">install </span>qemu-system-arm qemu-system-x86 qemu-system-misc
</code></pre></div></div>

<p><strong>Cross-compiling for ARM targets</strong></p>

<p>To build for ARM targets you will need a cross compiler:</p>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">sudo </span>apt-get <span class="nb">install </span>gcc-arm-linux-gnueabi g++-arm-linux-gnueabi
<span class="nb">sudo </span>apt-get <span class="nb">install </span>gcc-aarch64-linux-gnu g++-aarch64-linux-gnu
</code></pre></div></div>

<p>(you can install the hardware floating point versions as well if you wish)</p>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">sudo </span>apt-get <span class="nb">install </span>gcc-arm-linux-gnueabihf g++-arm-linux-gnueabihf
</code></pre></div></div>

<p><strong>Cross-compiling for RISC-V targets</strong></p>

<p>To build for RISC-V targets you will need a cross compiler:</p>

<ol>
  <li>
    <p>It is recommended to build the toolchain from source.</p>

    <div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code> git clone https://github.com/riscv/riscv-gnu-toolchain.git
 <span class="nb">cd </span>riscv-gnu-toolchain
 git submodule update <span class="nt">--init</span> <span class="nt">--recursive</span>
 <span class="nb">export </span><span class="nv">RISCV</span><span class="o">=</span>/opt/riscv
 ./configure <span class="nt">--prefix</span><span class="o">=</span><span class="s2">"</span><span class="k">${</span><span class="nv">RISCV</span><span class="k">}</span><span class="s2">"</span> <span class="nt">--enable-multilib</span>
 make linux
</code></pre></div>    </div>

    <p>After it is built, add the <code class="language-plaintext highlighter-rouge">$RISCV/bin</code> folder to your PATH. The built
 toolchain works for both 32-bit and 64-bit.</p>
  </li>
  <li>
    <p>Alternatively, any pre-built toolchain with multilib enabled should work.</p>
  </li>
</ol>

<p><strong>Builidng the seL4 manual</strong></p>

<p>If you would like to build the seL4 manual, you will need the following LaTeX pacakges:</p>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">sudo </span>apt-get <span class="nb">install </span>texlive texlive-latex-extra texlive-fonts-extra
</code></pre></div></div>

<h4 id="debian">Debian</h4>

<h5 id="for-debian-bullseye-or-later">For Debian Bullseye or later</h5>

<p>The dependencies listed in our Docker files <a href="https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles">repository</a> will work for a Debian installation. You can refer to this repository for an up-to-date list of base build dependencies. Specifically refer to the dependencies listed in the file here:</p>

<ul>
  <li><a href="https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles/blob/master/scripts/base_tools.sh">Base Tools</a></li>
  <li><a href="https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles/blob/master/scripts/sel4.sh">seL4</a></li>
  <li><a href="https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles/blob/master/scripts/apply-tex.sh">LaTeX</a></li>
</ul>

<h3 id="python-dependencies">Python Dependencies</h3>

<p>Regardless of your Linux distribution, python dependencies are required to build seL4, the manual and its proofs. To install you can run:</p>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code>pip3 <span class="nb">install</span> <span class="nt">--user</span> setuptools
pip3 <span class="nb">install</span> <span class="nt">--user</span> sel4-deps
</code></pre></div></div>

<p>(Some distributions use <code class="language-plaintext highlighter-rouge">pip</code> for python3, others use <code class="language-plaintext highlighter-rouge">pip3</code>.  Use the Python 3 version for your distribution)</p>

<h2 id="camkes-build-dependencies">CAmkES Build Dependencies</h2>

<p>To build a CAmkES based project on seL4, additional dependencies need to be installed on your host machine. Projects using CAmkES (the seL4 component system) need Haskell and some extra Python libraries in addition to the standard build tools. The following instructions cover the CAmkES build dependencies for Ubuntu/Debian. Please ensure you have installed the dependencies listed in sections <a href="#sel4-build-dependencies">seL4 Build Dependencies</a> and <a href="#get-googles-repo-tool">Get Google’s Repo tool</a> prior to building a CAmkES project.</p>

<h3 id="python-dependencies">Python Dependencies</h3>

<p>The Python dependencies required by the CAmkES build toolchain can be installed via pip:</p>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code>pip3 <span class="nb">install</span> <span class="nt">--user</span> camkes-deps
</code></pre></div></div>

<h3 id="haskell-dependencies">Haskell Dependencies</h3>

<p>The CAmkES build toolchain additionally requires Haskell. You can install the <a href="https://haskellstack.org">Haskell stack</a> on your distribution by running:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>curl -sSL https://get.haskellstack.org/ | sh
</code></pre></div></div>
<p>If you prefer not to bypass your distribution’s package manager, you can do</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>sudo apt-get install haskell-stack
</code></pre></div></div>

<h3 id="build-dependencies">Build Dependencies</h3>

<h4 id="ubuntu">Ubuntu</h4>

<p>These instructions are intended for Ubuntu LTS versions 20.04 and 22.04.</p>

<p>Install the following packages:</p>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">sudo </span>apt-get <span class="nb">install </span>clang gdb
<span class="nb">sudo </span>apt-get <span class="nb">install </span>libssl-dev libclang-dev libcunit1-dev libsqlite3-dev
<span class="nb">sudo </span>apt-get <span class="nb">install </span>qemu-kvm
</code></pre></div></div>

<h4 id="debian">Debian</h4>

<h5 id="for-debian-stretch-or-later">For Debian Stretch or later</h5>

<p>The dependencies listed in our docker files <a href="https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles">repository</a> will work for a Debian installation. You can refer to this repository for an up-to-date list of base build dependencies. Specifically refer to the dependencies listed in the:</p>

<ul>
  <li><a href="https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles/blob/master/camkes.dockerfile">CAmkES Dockerfile</a></li>
</ul>

<!--
     Copyright 2022, Proofcraft Pty Ltd
     Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)

     SPDX-License-Identifier: CC-BY-SA-4.0
-->

<!-- This file is also included on https://docs.sel4.systems/projects/buildsystem/host-dependencies.html  -->

<h1 id="proof-and-isabelle-dependencies">Proof and Isabelle Dependencies</h1>

<h2 id="proof-dependencies">Proof Dependencies</h2>

<h3 id="linux-packages---debian-bullseye">Linux Packages - Debian Bullseye</h3>

<p>On <strong>Debian Bullseye</strong>, to run all proofs you will need to install the following
packages:</p>

<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">sudo </span>apt-get <span class="nb">install</span> <span class="se">\</span>
    python3 python3-pip python3-dev <span class="se">\</span>
    gcc-arm-none-eabi gcc-aarch64-linux-gnu gcc-riscv64-unknown-elf <span class="se">\</span>
    build-essential libxml2-utils ccache <span class="se">\</span>
    ncurses-dev librsvg2-bin device-tree-compiler cmake <span class="se">\</span>
    ninja-build curl zlib1g-dev texlive-fonts-recommended <span class="se">\</span>
    texlive-latex-extra texlive-metapost texlive-bibtex-extra <span class="se">\</span>
    rsync
</code></pre></div></div>

<p>There is no package for the MLton compiler on Bullseye, so you will need to
install it from the <a href="http://www.mlton.org">MLton website</a>.</p>

<p>The Haskell Stack package is unavailable on Bullseye, so you will need to
install it from the <a href="https://docs.haskellstack.org/en/stable/">Haskell Stack
website</a>.</p>

<p>Continue with the <a href="#python">python setup step</a> below.</p>

<h3 id="linux-packages---ubuntu">Linux Packages - Ubuntu</h3>

<p>These instructions are intended for Ubuntu LTS versions 20.04, and 22.04.</p>

<p>To run all proofs you will need to install the following packages:</p>

<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">sudo </span>apt-get <span class="nb">install</span> <span class="se">\</span>
    python3 python3-pip python3-dev <span class="se">\</span>
    gcc-arm-none-eabi gcc-aarch64-linux-gnu gcc-10-riscv64-linux-gnu <span class="se">\</span>
    build-essential libxml2-utils ccache <span class="se">\</span>
    ncurses-dev librsvg2-bin device-tree-compiler cmake <span class="se">\</span>
    ninja-build curl zlib1g-dev texlive-fonts-recommended <span class="se">\</span>
    texlive-latex-extra texlive-metapost texlive-bibtex-extra <span class="se">\</span>
    mlton-compiler haskell-stack repo
</code></pre></div></div>

<p>Continue with the <a href="#python">python setup step</a> below.</p>

<h3 id="macos-packages">macOS packages</h3>

<p>The proofs work well on Intel and Apple Silicon Macs.</p>

<p>These instructions use Homebrew, which can be installed from <a href="https://brew.sh">their website</a>.
To install the main dependencies and cross compilers, use the following steps:</p>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code>brew <span class="nb">install </span>git libxml2 ncurses librsvg dtc cmake ninja texlive rsync python ccache <span class="se">\</span>
     zstd haskell-stack mlton arm-none-eabi-gcc repo

brew <span class="nb">install</span> <span class="nt">--cask</span> gcc-arm-embedded

brew tap messense/macos-cross-toolchains
brew <span class="nb">install </span>x86_64-unknown-linux-gnu aarch64-unknown-linux-gnu

brew tap riscv/riscv
brew <span class="nb">install </span>riscv-tools
</code></pre></div></div>

<p>The instructions in the sections below apply for both Linux and macOS.</p>

<h3 id="python">Python</h3>

<p>The build system for the seL4 kernel requires several python packages:</p>

<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>pip3 <span class="nb">install</span> <span class="nt">--user</span> <span class="nt">--upgrade</span> pip
pip3 <span class="nb">install</span> <span class="nt">--user</span> sel4-deps
</code></pre></div></div>

<h3 id="haskell-stack">Haskell Stack</h3>

<p>After installing <a href="https://docs.haskellstack.org/en/stable/">haskell-stack</a>
(already included in the packages above on Mac and Ubuntu), make sure you’ve
adjusted your <code class="language-plaintext highlighter-rouge">PATH</code> to include <code class="language-plaintext highlighter-rouge">$HOME/.local/bin</code>, that you’re running an
up-to-date version, and that you have installed cabal:</p>

<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>stack upgrade <span class="nt">--binary-only</span>
which stack <span class="c"># should be $HOME/.local/bin/stack</span>
stack <span class="nb">install </span>cabal-install
</code></pre></div></div>

<h2 id="checking-out-the-repository-collection">Checking out the repository collection</h2>

<p>The seL4 repositories use the <a href="https://gerrit.googlesource.com/git-repo/+/HEAD/README.md">Google <code class="language-plaintext highlighter-rouge">repo</code> tool</a> for configuration
control and managing sets of repositories. For verification, this means in
particular managing the correct combinations of the proofs, the kernel sources,
and the Isabelle/HOL theorem prover.</p>

<p>The <a href="https://github.com/seL4/verification-manifest">verification-manifest</a> repository records which versions of these are known
to work well together.</p>

<p>To check out a consistent set of repositories, run the following steps:</p>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">mkdir </span>verification
<span class="nb">cd </span>verification
repo init <span class="nt">-u</span> https://git@github.com/seL4/verification-manifest.git
repo <span class="nb">sync</span>
</code></pre></div></div>

<p>If you are developing proofs, intending to contribute, and have <code class="language-plaintext highlighter-rouge">ssh</code> set up
for GitHub, use</p>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code>repo init <span class="nt">-m</span> devel.xml <span class="nt">-u</span> ssh://git@github.com/seL4/verification-manifest.git
</code></pre></div></div>

<p>instead for the <code class="language-plaintext highlighter-rouge">init</code> line. The <code class="language-plaintext highlighter-rouge">-m devel.xml</code> gives you the <code class="language-plaintext highlighter-rouge">master</code> branch of
the <code class="language-plaintext highlighter-rouge">l4v</code> repository instead of the last known-good version. To set up <code class="language-plaintext highlighter-rouge">git</code> for
<code class="language-plaintext highlighter-rouge">ssh</code> make sure to use the <code class="language-plaintext highlighter-rouge">ssh://</code> protocol explicitly as above instead of just
<code class="language-plaintext highlighter-rouge">git@github.com</code>, because the short form seems to confuse <code class="language-plaintext highlighter-rouge">repo</code>.</p>

<p>If you are looking to use the proofs for a specific release version of seL4, use
the <code class="language-plaintext highlighter-rouge">-m</code> option to select the corresponding manifest file in the
<a href="https://github.com/seL4/verification-manifest">verification-manifest</a> repository.</p>

<h2 id="isabelle-setup">Isabelle Setup</h2>

<p>After the repository is set up using <code class="language-plaintext highlighter-rouge">repo</code> with the <a href="https://github.com/seL4/verification-manifest">verification-manifest</a>
repository, you should have following directory structure, where <code class="language-plaintext highlighter-rouge">l4v</code> is the
repository you are currently looking at:</p>

<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>verification/
    HOL4/
    graph-refine/
    isabelle/
    l4v/
    seL4/
</code></pre></div></div>

<p>To set up Isabelle for use in <code class="language-plaintext highlighter-rouge">l4v/</code>, assuming you have no previous
installation of Isabelle, run the following commands in the directory
<code class="language-plaintext highlighter-rouge">verification/l4v/</code>:</p>

<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">mkdir</span> <span class="nt">-p</span> ~/.isabelle/etc
<span class="nb">cp</span> <span class="nt">-i</span> misc/etc/settings ~/.isabelle/etc/settings
./isabelle/bin/isabelle components <span class="nt">-a</span>
./isabelle/bin/isabelle jedit <span class="nt">-bf</span>
./isabelle/bin/isabelle build <span class="nt">-bv</span> HOL
</code></pre></div></div>

<p>These commands perform the following steps:</p>

<ul>
  <li>create an Isabelle user settings directory.</li>
  <li>install L4.verified Isabelle settings.
These settings initialise the Isabelle installation to use the standard
Isabelle <code class="language-plaintext highlighter-rouge">contrib</code> tools from the Munich Isabelle repository and set up
paths such that multiple Isabelle repository installations can be used
side by side without interfering with each other.</li>
  <li>download <code class="language-plaintext highlighter-rouge">contrib</code> components from the Isabelle repository. This includes
Scala, a Java JDK, PolyML, and multiple external provers. You should
download these, even if you have these tools previously installed
elsewhere to make sure you have the right versions. Depending on your
internet connection, this may take some time.</li>
  <li>compile and build the Isabelle PIDE jEdit interface.</li>
  <li>build basic Isabelle images to ensure that
the installation works. This may take a few minutes.</li>
</ul>

<p>Alternatively, it is possible to use the official Isabelle2022 release
bundle for your platform from the <a href="https://isabelle.in.tum.de">Isabelle website</a>. In this case, the
installation steps above can be skipped, and you would replace the directory
<code class="language-plaintext highlighter-rouge">verification/isabelle/</code> with a symbolic link to the Isabelle home directory
of the release version. Note that this is not recommended for development,
since Google repo will overwrite this link when you synchronise repositories
and Isabelle upgrades will have to be performed manually as development
progresses.</p>

<p>You are now set up to process proofs, for instance by following the instructions
at the bottom of the main <a href="https://github.com/seL4/l4v/blob/master/README.md#running-the-proofs">README page</a>.</p>

<p>The sections below contain a few tools and tips for proof development on seL4.</p>

<h2 id="pide-tools">PIDE Tools</h2>

<p>The following tools and tips can make writing proofs easier and more efficient
when using the Isabelle PIDE jEdit interface.</p>

<h3 id="whitespace-plugin">WhiteSpace plugin</h3>

<p>The WhiteSpace plugin can highlight normally invisible whitespace characters
such as tabs and spaces, and can remove trailing whitespace on save. To
install and configure the WhiteSpace plug-in for jEdit, follow
the instructions below.</p>

<ol>
  <li>Go to Plugins -&gt; Plugin manager -&gt; Install.</li>
  <li>Search for <code class="language-plaintext highlighter-rouge">WhiteSpace</code> and install the plugin.</li>
  <li>Go to Plugins -&gt; Plugin Options -&gt; WhiteSpace -&gt; On save actions.</li>
  <li>Check “Remove trailing whitespace” and click Apply.</li>
</ol>

<h3 id="key-bindings-for-navigator">Key bindings for Navigator</h3>

<p>The Isabelle PIDE provides “Back” and “Forward” actions that allow you to
easily navigate to previous positions in your edit history. Follow the steps
below to bind a key to the “Back” function. We recommend <code class="language-plaintext highlighter-rouge">[ctrl]+[`]</code>.</p>

<ol>
  <li>Go to Utilities -&gt; Global Options -&gt; jEdit -&gt; Shortcuts.</li>
  <li>Select Action Set -&gt; Plugin: Navigator.</li>
  <li>Set a shortcut for <code class="language-plaintext highlighter-rouge">Back</code>.</li>
</ol>

<h3 id="go-to-error-macro">Go-to-error macro</h3>

<p>Run the following commands in the directory <code class="language-plaintext highlighter-rouge">verification/l4v/</code>:</p>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">mkdir</span> <span class="nt">-p</span> ~/.isabelle/jedit/macros
<span class="nb">cp </span>misc/jedit/macros/goto-error.bsh ~/.isabelle/jedit/macros/.
</code></pre></div></div>

<p>You can add keybindings for this macro in the usual way, by going to
<code class="language-plaintext highlighter-rouge">Utilities -&gt; Global Options -&gt; jEdit -&gt; Shortcuts</code>.</p>

<p>Additionally, our fork of Isabelle/jEdit has an updated indenter which is more
proof-context aware than the ‘original’ indenter. Pressing <code class="language-plaintext highlighter-rouge">ctrl+i</code> while some
<code class="language-plaintext highlighter-rouge">apply</code>-script text is selected should auto-indent the script while respecting
subgoal depth and maintaining the relative indentation of multi-line <code class="language-plaintext highlighter-rouge">apply</code>
statements.</p>


  </div>







  
    
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
    <ul id="toc" class="section-nav">
<li class="toc-entry toc-h2"><a href="#get-googles-repo-tool">Get Google’s Repo tool</a></li>
<li class="toc-entry toc-h2"><a href="#sel4-build-dependencies">seL4 Build Dependencies</a>
<ul>
<li class="toc-entry toc-h3"><a href="#base-build-dependencies">Base Build Dependencies</a>
<ul>
<li class="toc-entry toc-h4"><a href="#ubuntu">Ubuntu</a></li>
<li class="toc-entry toc-h4"><a href="#debian">Debian</a>
<ul>
<li class="toc-entry toc-h5"><a href="#for-debian-bullseye-or-later">For Debian Bullseye or later</a></li>
</ul>
</li>
</ul>
</li>
<li class="toc-entry toc-h3"><a href="#python-dependencies">Python Dependencies</a></li>
</ul>
</li>
<li class="toc-entry toc-h2"><a href="#camkes-build-dependencies">CAmkES Build Dependencies</a>
<ul>
<li class="toc-entry toc-h3"><a href="#python-dependencies">Python Dependencies</a></li>
<li class="toc-entry toc-h3"><a href="#haskell-dependencies">Haskell Dependencies</a></li>
<li class="toc-entry toc-h3"><a href="#build-dependencies">Build Dependencies</a>
<ul>
<li class="toc-entry toc-h4"><a href="#ubuntu">Ubuntu</a></li>
<li class="toc-entry toc-h4"><a href="#debian">Debian</a>
<ul>
<li class="toc-entry toc-h5"><a href="#for-debian-stretch-or-later">For Debian Stretch or later</a></li>
</ul>
</li>
</ul>
</li>
</ul>
</li>
<li class="toc-entry toc-h2"><a href="#proof-dependencies">Proof Dependencies</a>
<ul>
<li class="toc-entry toc-h3"><a href="#linux-packages---debian-bullseye">Linux Packages - Debian Bullseye</a></li>
<li class="toc-entry toc-h3"><a href="#linux-packages---ubuntu">Linux Packages - Ubuntu</a></li>
<li class="toc-entry toc-h3"><a href="#macos-packages">macOS packages</a></li>
<li class="toc-entry toc-h3"><a href="#python">Python</a></li>
<li class="toc-entry toc-h3"><a href="#haskell-stack">Haskell Stack</a></li>
</ul>
</li>
<li class="toc-entry toc-h2"><a href="#checking-out-the-repository-collection">Checking out the repository collection</a></li>
<li class="toc-entry toc-h2"><a href="#isabelle-setup">Isabelle Setup</a></li>
<li class="toc-entry toc-h2"><a href="#pide-tools">PIDE Tools</a>
<ul>
<li class="toc-entry toc-h3"><a href="#whitespace-plugin">WhiteSpace plugin</a></li>
<li class="toc-entry toc-h3"><a href="#key-bindings-for-navigator">Key bindings for Navigator</a></li>
<li class="toc-entry toc-h3"><a href="#go-to-error-macro">Go-to-error macro</a></li>
</ul>
</li>
</ul>
</div>

  
  
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
  
    <ul class="section-nav">
    	<h2> seL4 Buildsystem </h2> 
        <li>
          
          <a style="" class="" href="/projects/buildsystem/">
            Documentation homepage
          </a>
        </li>

















    
        <h3>Repositories</h3>
    
        <li>
          <a class="" href="https://github.com/sel4/sel4">
            sel4
          </a>
        </li>

    
        <li>
          <a class="" href="https://github.com/sel4/sel4_tools">
            sel4_tools
          </a>
        </li>









  







    
        <h3>Recent Updates</h3>
    
        <li>
          <a style="" href="/updates/buildsystem/11.0.x.html">
            seL4 11.0.x-compatible
          </a>
        </li>

    </ul>

</div>


</div>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
                Page last updated: Mon Sep 23 12:58:08 2024 +0200 7c251159a6
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/projects/buildsystem/host-dependencies.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/projects/buildsystem/host-dependencies.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
